package tr.edu.ege.kipler.satisfiability.completion.rules.dl;

import java.util.Iterator;

import tr.edu.ege.kipler.satisfiability.BranchingException;
import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.Reasoner;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.blocking.BlockingStrategy;
import tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism.UnionBranchingPoint;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.ConceptCategory;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept;
import tr.edu.ege.kipler.syntax.concept.Concept;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class UnionRule extends ABoxRule {

	private boolean applied;

	private Reasoner prover;

	private ABox aBox;

	private BlockingStrategy blocking;

	public UnionRule(Reasoner prover, BlockingStrategy blocking) {
		this.prover = prover;
		setBlocking(blocking);
	}

	public BlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(BlockingStrategy blocking) {
		this.blocking = blocking;
	}

	public boolean isApplied() {
		return applied;
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual().conceptIterator(
					ConceptCategory.UNION); i.hasNext();) {
				Concept concept = i.next();
				BinaryConcept bd = (BinaryConcept) concept;
				if (!getIndividual().contains(bd.getLhs())
						&& !getIndividual().contains(bd.getRhs())) {
					branchForConcepts(bd);
					applied = true;
					throw new BranchingException();
				}
			}
		}
	}

	private void branchForConcepts(BinaryConcept bd)
			throws UnsatisfiableException {
		ConceptAssertion assert1 = new ConceptAssertion(bd.getLhs(),
				getIndividual().getName());
		ConceptAssertion assert2 = new ConceptAssertion(bd.getRhs(),
				getIndividual().getName());
		UnionBranchingPoint bp = new UnionBranchingPoint();
		bp.setWcs(getWcs());
		bp.setWorld(getWorld());
		bp.addFormula(assert1);
		bp.addFormula(assert2);
		bp.setBranchCause(new ConceptAssertion(bd, getIndividual().getName()));
		prover.addBranch(bp);
		getWcs().getData().getLogger().info(
				"WCS " + getWcs().getId() + " Union rule: Branching for "
						+ assert1 + " and " + assert2);

	}

}
